  \documentclass{beamer}

%\usepackage{pgfpages}
%\setbeameroption{show notes}
%\setbeameroption{show notes on second screen=right}
\usepackage[utf8]{inputenc}
\usepackage{amsmath,amssymb,amsthm, amsfonts} 
\usepackage{mathpartir}
\usepackage{textcomp}
\usepackage{stmaryrd}
\usepackage{myproof}

%\usepackage[latin1]{inputenc}
%\usepackage[T1]{fontenc}
%\usepackage{pgfpages}

\usepackage{times}
\usepackage{xspace}

\usepackage[english]{babel}
\usepackage{url}

\usepackage{wrapfig}
\usepackage{davidemacro}
\usepackage{evolvablemacro}


\usepackage{color}
\newcommand{\emphcolor}[1]{\textcolor{magenta}{#1}\xspace}



\title[Adaptable Processes]{Disciplined Structured Communications with
Consistent Runtime Adaptation}
\author[Cinzia Di Giusto]{Cinzia Di Giusto}
\date[]{}
  
\institute[CEA]{CIRM, Marseille}

\setbeamertemplate{navigation symbols}{} 

\usecolortheme{crane}
\useoutertheme{progressbar}
\useinnertheme{progressbar}
\usefonttheme{progressbar}

%\usetheme{progressbar}

\usepackage{setspace}

\newcommand{\putat}[3]{\begin{picture}(0,0)(0,0)\put(#1,#2){#3}\end{picture}}

\newcommand{\emphcolorb}[1]{\textcolor{blue}{#1}\xspace}


%red, gray,
%orange,
%green, white, pink,
%blue, darkgray,
%cyan,	magenta,	yellow,	black, lightgray,	brown,	lime,	olive,
%purple,

\newcommand{\tealtext}[1]{\textcolor{teal}{#1}\xspace}

\newcommand{\str}[1]{\structure{#1}}

\progressbaroptions{headline=sections,frametitle=normal}


% Context
\newcommand{\ol}{\langle\!\langle}
\newcommand{\cl}{\rangle\!\rangle}
\newcommand{\hl}[1]{\ol #1 \cl}
\newcommand{\fillcon}[2]{\ensuremath{#1\hl{#2}}}

\newcommand{\pired}{\longrightarrow}
\newcommand{\arro}[1]{\xrightarrow[]{#1}}

\newcommand{\rulename}[1]{\textsc{(#1)}}

\newcommand{\nm}[1]{\ensuremath{\mathsf{#1}}}
 \newcommand{\nmu}[1]{\ensuremath{\mathtt{#1}}}
 \newcommand{\midef}{\ensuremath{\stackrel{\mathsf{def}}{=}}}



%\newcommand{\str}[1]{\structure{#1}}
\newcommand{\fkspc}{{\tiny \ }\\}



\begin{document}

\begin{frame}


 \titlepage
\end{frame}

%
%\begin{frame}
% \frametitle{This work}
%
%
%\begin{itemize}
%
%\item Journal version:
%
%\begin{block}{}
%{\tiny
%M. Bravetti, C. Di Giusto, J.A. P\`erez and G. Zavattaro. \\Adaptable processes Accepted for publication in Logical Methods for Computer Science.
%}
%\end{block}
%
% \item Based on following works:
%\begin{block}{}
%{\tiny
%-- M. Bravetti, C. Di Giusto, J.A. P\`erez and G. Zavattaro. \\Adaptable processes (Extended Abstract). FMOODS-FORTE 2011, LNCS, vol. 6722 pages 90--105}
%
% {\tiny
%-- M. Bravetti, C. Di Giusto, J.A. P\`erez and G. Zavattaro.\\ Towards the Verification of Adaptable Processes. ISoLA 2012, LNCS, vol. 7609 pages 269-283, 2012
%}
%
%{\tiny
%--  C. Di Giusto and J.A. P\`erez.\\ Disciplined Structured Communications with
%Consistent Runtime Adaptation. To appear in SAC 2013.
%}
%\end{block}
%
% \item Papers available at  
%\emphcolor{\url{www.cs.unibo.it/~perez/ap/}}  
%
%\end{itemize}
%
%
%\end{frame}

\section{Motivation}

\begin{frame}
   \frametitle{Our target}
  

   
   \begin{block}{}
   \begin{center}
     We are interested in modeling and reasoning about systems that can \\
     \emphcolor{evolve dynamically}\\ without requiring a shutdown of the whole system.    
   \end{center}
   \end{block}
 
 \vspace{0.5cm}
 \begin{center}
  \includegraphics[scale=0.05]{Target1.png}
 \end{center}

 \end{frame}
 
 
 \begin{frame}
 
 \frametitle{Scenario}
 
 
 \begin{enumerate}
  \item Systems that can \emphcolor{dynamically update} their parts: i.e. APT for Debian/Ubuntu Linux, software updates for Apple, \dots
  
  \vspace{0.7cm}
  
  \item  Systems that can \emphcolor{adapt} themselves to changed circumstances:
  \begin{itemize}
    \item to \emphcolor{react to an error}, evolution as a way of correcting faults,
    
    \vspace{0.2cm}
    
    \item to \emphcolor{respond to a change} in the environment, systems can adapt to user context.   
   \end{itemize}
   

   
 \end{enumerate}
 
\end{frame}




\begin{frame}
\frametitle{Example: Scaling in cloud computing}
\only<1-3>{\putat{260}{-5}{\includegraphics[scale=0.16]{amazon-cloud.png}}}
\vspace{-5mm}
\begin{center}
\emphcolor{Auto Scaling}
\end{center}


\begin{columns}[b]
\begin{column}{0.5\textwidth}
 \only<1>{\includegraphics[width = 0.8\textwidth]{cloudnetworkter.jpg}  }
\only<2->{\includegraphics[width = 0.8\textwidth]{cloudnetworkalert.jpg}  }
\end{column}
\begin{column}{0.5\textwidth}
\only<3->{ \includegraphics[width = 0.8\textwidth]{cloudnetworkbis.jpg}
\putat{-170}{25}{\includegraphics[scale=0.14]{arrow.png}}  
\putat{-20}{10}{\includegraphics[scale=0.45]{validate.png}}  
}
\end{column}


\end{columns}

\only<4->{
\begin{center}
 \small
 A property to guarantee: every scaling alert  will disappear after a bounded amount of time, i.e. the scaling request is promptly addressed by the cloud provider. 
 \end{center}


 
}
\end{frame}




\begin{frame}
 \frametitle{Our Proposal}
 
 

\begin{block}{}
\centering
\begin{itemize}
 \item A \emphcolor{model} of evolvable systems by means of process algebras
 
 \vspace{0.5cm}
 \item A \emphcolor{framework} for verifying properties of those systems. 
\end{itemize}


 
 \end{block}

\end{frame}



\begin{frame}
 \frametitle{Why a new process calculus?}
 


Concurrency is often associated to dynamic behaviors:

\vspace{0.2cm}

\begin{itemize}
  \item In the $\pi$-calculus, \emphcolor{dynamic network topologies} are obtained through channel/link mobility.

    \vspace{0.2cm}
  \item In the Ambient calculus, \emphcolor{dynamic spatial topologies} are obtained through ambient  mobility.

\end{itemize}

\end{frame}


\begin{frame}
\frametitle{But \dots}

\begin{itemize}
 \item Neither $\pi$ nor Ambient can describe changes that occur at the process level.
\vspace{0.2cm}
 \item They cannot influence the evolution of the process along time.
\end{itemize}

\vspace{0.5cm}
\pause
\begin{block}{}
We need a mechanism so that processes can be 
\begin{itemize}
 \item Stopped
 \item Restarted
 \item \emphcolor{Modified}
\end{itemize}
 
\end{block}

 

\end{frame}







\begin{frame}

\frametitle{Our approach}
%A \str{} to the analysis of \str{evolvable systems} 


We are mainly concerned with \emphcolor{dynamic reconfiguration} issues:\\
\vspace{0.2cm}
\begin{itemize}
\item finding proper \emphcolor{evolution/reconfiguration} mechanisms,
\vspace{0.2cm}
\item understanding the \emphcolor{properties} evolvable systems should ensure, 
\vspace{0.2cm}
\item statically \emphcolor{identifying} the good processes.
\end{itemize}
 
\end{frame}

\begin{frame}
 
 \frametitle{Our proposal}
\begin{itemize}
\item A \emphcolor{process calculus} of adaptable processes, called \emphcolorb{\evol{}} 
\vspace{0.2cm}
\item \emphcolor{Verification language} $\mathcal{L}$ for evolvable systems defined in \evol{} 
\vspace{0.2cm}
\item \emphcolor{(Un)decidability results} for the properties expressed in $\mathcal{L}$
\vspace{0.2cm}
\item A \emphcolor{Type system} to sort out well formed processes
\end{itemize}
 
\end{frame}


\section{Calculi}

\begin{frame}
\frametitle{Inspirations}

As we need a mechanism that handles processes:
\vspace{0.2cm}

\begin{itemize}
 \item we looked  at \emphcolor{process passing} calculi (Higher Order $\pi$)
\vspace{0.2cm}
 \item we borrowed inspiration (in particular) from the \emphcolor{suspension operator} of the Kell-calculus
\vspace{0.2cm}
\item In Kell, processes can be suspended and then sent along a channel 

\end{itemize}
\end{frame}


\begin{frame}
\frametitle{A calculus for adaptable processes}

CCS without restriction

  \begin{itemize} 
    \item \emphcolor{Input/Output}: $\qquad \quad \ \ a.P \qquad \outC{a}.P$
    \item \emphcolor{Parallel composition}:  $\ P_1 \parallel P_2$
    \item \emphcolor{Recursion}: $  rec X . P$ 
  \end{itemize}



\end{frame}

\begin{frame}
 \frametitle{Semantics}

\begin{itemize}
  \item Input/output synchronization:

\only<1>{$$a.P_1 \parallel \outC{a}.P_2$$ }
\only<2>{$$\emphcolorb{a}.P_1 \parallel \emphcolorb{\outC{a}}.P_2$$ }
\only<3->{$$\emphcolorb{a}.P_1 \parallel \emphcolorb{\outC{a}}.P_2 \pired P_1 \parallel P_2$$ }
\vspace{0.5cm}
 \only<4->{ \item Recursion: $rec X .P \arro{~\alpha~}  P\sub{rec X. P}{X}$} 
\end{itemize}  
\end{frame}


\begin{frame}
  \frametitle{The construct for adaptability}
  
  \begin{itemize}
  \item \emphcolor{Localities}: $\component{l}{P}$
  \end{itemize}
  \begin{center}
  $\component{l}{P}$ is the \emphcolor{adaptable process} $P$ located at name $l$
    \end{center}
\begin{block}{}
Localities are \emphcolor{transparent}:
$ \qquad \cfrac {P \xrightarrow{~\alpha~} P'} 
 			{\component{l}{P} \xrightarrow{~\alpha~}  \component{l}{P'}}	$
\vspace{0.25cm} 			
 			
\end{block}  
  

  \pause
  \begin{itemize}
  \item \emphcolor{Update prefixes}: $\update{l}{U}$
  \end{itemize}
\begin{center}
$U$ is a \emphcolor{context}, with zero or more holes, denoted $\bullet$
\end{center}
\end{frame}


\begin{frame}
 \frametitle{How to update a process}
 
 \begin{block}{Reconfiguration}
\begin{itemize}

\item Dynamic reconfiguration is obtained  via an interaction  with update prefixes:
$$
\component{l}{P} \parallel \update{l}{U}.Q \xrightarrow{~\tau~} \fillcon{U}{P} \parallel Q
$$

\item{Process $\fillcon{U}{P}$ is obtained by filling in the holes in $U$ with $P$}
\end{itemize}
\end{block}
\pause
\begin{example}

\only<2>{$$ \component{l}{P_1} \parallel \update{l}{P_2 \parallel \bullet}.Q  $$}
\only<3>{$$ \component{\emphcolor{l}}{P_1} \parallel \update{\emphcolor{l}}{P_2 \parallel \bullet}.Q  $$}
\only<4 >{$$ \component{l}{\emphcolorb{P_1}} \parallel \update{l}{P_2 \parallel \emphcolorb{\bullet} }.Q  $$}
\only<5 >{$$ \component{l}{P_1} \parallel \update{l}{P_2 \parallel \bullet }.Q \pired \emphcolorb{P_2 \parallel P_1} \parallel Q  $$}
\end{example}

\end{frame}




\begin{frame}
\frametitle{A calculus for adaptable processes }

\begin{block}{}
CCS without restriction \only<2->{plus \emphcolor{localities}}\only<3->{ and \emphcolorb{update prefixes}:}
$$
\begin{array}{ll}
P        ::=& \pi.P   \, \mid \, 
          P \parallel P  \, \mid \,  rec X.P \, \mid \, X \, \only<2->{\mid \, \emphcolor{\component{l}{P}}} \, \mid \, \only<3->{\emphcolorb{x}}\\ \\
\pi   ::=&  a \, \mid \, \outC{a} \only<3->{\, \mid \, \emphcolorb{\update{l}{P(x)}}} 
\end{array}
$$
\end{block}

\end{frame}








\frame{
\frametitle{A first example}

A basic client-server scenario:   
\begin{align*}
\only<1>{& \componentbbig{client}{\component{run}{P} \parallel \outC{upd}} \parallel \componentbbig{server}{upd.\update{run}{\component{run}{Q \parallel old.x}}.S} \\ }
\only<2>{& \componentbbig{client}{\component{run}{P} \parallel \emphcolor{\outC{upd}}} \parallel \componentbbig{server}{\emphcolor{upd}.\update{run}{\component{run}{Q \parallel old.x}}.S} \\ }
\only<3->{& \textcolor{gray}{ \componentbbig{client}{\component{run}{P} \parallel \outC{upd}} \parallel \componentbbig{server}{upd.\update{run}{\component{run}{Q \parallel old.x}}.S}} \\ \\} 
\only<3>{\pired ~ & \componentbbig{client}{\component{run}{P}} \parallel \componentbbig{server}{\update{run}{\component{run}{Q \parallel old.x}}.S} \\ }
\only<4>{\pired ~ & \componentbbig{client}{\component{\emphcolorb{run}}{P}} \parallel \componentbbig{server}{\update{\emphcolorb{run} }{\component{run}{Q \parallel old.x}}.S} \\ }
\only<5>{\pired ~ & \componentbbig{client}{\component{run}{\emphcolorb{P}}} \parallel \componentbbig{server}{\update{run }{\component{run}{Q \parallel old.\emphcolorb{x}}}.S} \\}
\only<6>{
\textcolor{gray}{\pired} ~ & \textcolor{gray}{\componentbbig{client}{\underbrace{\component{run}{P}}}  \parallel \componentbbig{server}{\update{run }{\component{run}{Q \parallel old.x}}.S}} \\
\\
\pired ~ & \componentbbig{client}{\component{run}{Q \parallel old.P} }  \parallel \componentbbig{server}{S}}
\end{align*}

}

\begin{frame}
\frametitle{Some evolvability patterns}
\begin{itemize}
\item<1->\emphcolorb{Deep update}
 $$\componentbbig{a}{Q \parallel \component{b}{R \parallel \emphcolor{\component{c}{S_{1}}}\, }\, } \parallel \update{c}{\component{d}{S_2}}.\nil \pired \componentbbig{a}{Q \parallel \componentbbig{b}{R \parallel \emphcolor{\component{d}{S_{2}}}\, }\, } \parallel \nil $$
\item<2->\emphcolorb{Destroyer}$$ \component{a}{P} \parallel \update{a}{Q}.R \pired Q \parallel R \quad (x \not \in Q)$$
\item<3>\emphcolorb{Plug-in} $$\component{a}{Q} \parallel \update{a}{\component{a}{c{.}x +R}}.\nil \pired \component{a}{c{.}Q +\fillcon{R}{Q}} \parallel \nil$$ 
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Some evolvability patterns}
\begin{itemize}
\item<1->\emphcolorb{Renaming} $$\component{m}{\component{a}{Q}} \parallel \component{n}{\update{a}{\component{b}{x}}.S} \pired \component{m}{\component{b}{Q} }\parallel \component{m}{S}$$
\item<2->\emphcolorb{Backup} $$\component{a}{Q} \parallel \update{a}{\component{a}{x} \parallel \component{b}{x}}.S \pired \component{a}{Q} \parallel \component{b}{Q} \parallel S$$
\item<3>\emphcolorb{Replacement} $$ \component{a}{Q} \parallel \update{a}{\component{a}{R}}.S \pired \component{a}{R} \parallel S  ~~(x \not \in R)$$ 
\end{itemize}
\end{frame}









\section{Properties}





\begin{frame}
\frametitle{Verification problems for adaptable processes}

An evolvable system is composed of:
\vspace{0.2cm}
\begin{itemize}
 \item an \emphcolor{initial configuration} $P$ 
\vspace{0.2cm}
 \item an arbitrary number of \emphcolorb{reconfigurations} $\mathcal{M}$
\end{itemize}
 \vspace{0.5cm}

\pause
\begin{itemize}
 \item We observe the system's behavior using \emphcolor{inputs and outputs}. 
\vspace{0.2cm}
 \item These observables represent \emphcolor{special signals}: errors, interrupts.

\end{itemize}



\end{frame}


\begin{frame}
\frametitle{Correctness in an evolvable scenario}
\only<1>{\includegraphics[height=50mm]{cluster0.pdf}}
\only<2>{\includegraphics[height=50mm]{cluster2.pdf}}
\only<3>{\includegraphics[height=50mm]{cluster1.pdf}}
\only<4>{\includegraphics[height=50mm]{cluster3.pdf}}
\only<5>{\includegraphics[height=50mm]{cluster4.pdf}}
\end{frame}








\begin{frame}
\frametitle{Verification problems for adaptable processes}
\putat{280}{15}{\includegraphics[scale=0.12]{Certificazione-qualita.png}}

Given:
\begin{itemize}
 \item an initial configuration $P$, 
 \item a set of reconfigurations,
 \item a special error signal $e$.
\end{itemize}

\vspace{0.2cm}
\begin{block}{}
\centering 
We would like to know if  for every reachable configuration exposing $e$ the system recovers in at most $k$ steps.\end{block}
\end{frame}






\begin{frame}
\frametitle{Example: Scaling in cloud computing}
\putat{260}{-5}{\includegraphics[scale=0.16]{amazon-cloud.png}}
\vspace{-5mm}
\begin{center}
\emphcolor{Auto Scaling}
\end{center}
\vspace{5mm}

\begin{columns}[b]
\begin{column}{0.5\textwidth}
\includegraphics[width = 0.8\textwidth]{cloudnetworkalert.jpg}  
\end{column}
\begin{column}{0.5\textwidth}
 \includegraphics[width = 0.8\textwidth]{cloudnetworkbis.jpg}
\putat{-170}{25}{\includegraphics[scale=0.14]{arrow.png}}  
\putat{-20}{10}{\includegraphics[scale=0.45]{validate.png}}  
\end{column}


\end{columns}


\end{frame}




\begin{frame}
 \frametitle{Generalization of the verification properties}
\begin{block}{} 
 \centering
\begin{spacing}{2}
\vspace{1em}
Properties can be expressed in a proper \emphcolor{temporal logic}
over adaptable processes.
\end{spacing}
\end{block}
\pause
\vspace{0.5cm}
\begin{definition}[The logic: \emphcolor{\Log}]
 $
  \phi ::=  \alpha \sep T \sep \phi\forr\phi \sep \phi\fand\phi \sep\fneg\phi \sep \di\phi \sep \ev\phi 
$
 
  
 \end{definition}

\end{frame}





\begin{frame}
 \frametitle{Some formulae}
 
\begin{itemize}
\item<1->\emphcolorb{k consecutive errors} $$\mathsf{CB}_{k}(e) \defi \neg  \ev \big(\underbrace{e \fand  \di(e \fand \di(e \fand \ldots \fand \di e))}_{\text{$e$ appears $k$ times}} \big)$$
\item<2>\emphcolorb{monotone correctness} 
$$
\mathsf{MC}(e) \defi \neg \ev \big( e \fand \di \ev(\neg e \fand \di \ev e) \big)
$$
\end{itemize}

\end{frame}



\begin{frame}
 \frametitle{Undecidability of the logic}

\begin{itemize}
 \item Formulae in $\Lo$ are \emphcolor{undecidable} in \evol{}.
\vspace{0.5cm}

 \item The satisfiability problem can be related to \emphcolor{termination} in Turing Complete models
\vspace{0.5cm}
 \item Given a Turing machine $M$,  its encoding into \evol{} can signal termination through a special observable
 
\end{itemize}
\end{frame}



\begin{frame}
 \frametitle{Towards decidability}

\begin{itemize}
 \item \emphcolor{Intuition}: two orthogonal approaches
 \begin{itemize}
 \item[-] to weaken the logic
 
 \item[-] to disallow some update patterns.
 
 \end{itemize}
 
 
 

%i.e. holes cannot appear behind prefixes
\vspace{0.5cm}
 \item Obtain fragments that are powerful enough to model interesting scenarios 

\end{itemize}
\end{frame}





\begin{frame}
 \frametitle{The restricted logic}
 
 
 \begin{definition}[$\Lo_r$]
 The restricted logic is composed by formulae of the form $\phi$ and $\neg \phi$ where $\phi$ does not contain any negation
  
 \end{definition}

 \vspace{0.5cm}
 \pause
 
 
 \begin{block}{Properties in $\Lo_r$}
 \emphcolorb{k consecutive errors} $$\mathsf{CB}_{k}(e) \defi \neg  \ev \big(\underbrace{e \fand  \di(e \fand \di(e \fand \ldots \fand \di e))}_{\text{$e$ appears $k$ times}} \big)$$
  
  
 \end{block}

 
\end{frame}



\begin{frame}
\frametitle{The table:} 
\begin{center}
\begin{tabular}{c|c|c}
		& $\Lo$ & $\Lo_r$ \\
\hline \hline
\evol{1}	& undec  ~& ~ undec~\\

\end{tabular}
\end{center}

\end{frame}



\begin{frame}
 \frametitle{Fragments: Ungarded \evol{2}} 

\begin{itemize}
 \item Variables cannot appear behind prefixes

\vspace{0.5cm}
\pause

 \item \evol{2} is weakly Turing powerful
\vspace{0.5cm}

\item The encoding has 
an infinite sequence of  runs if and only 
if the corresponding \mm terminates. 

\vspace{0.5cm}
\item Termination can be related to the satisfiability  of formulae

\end{itemize}

\end{frame}


\begin{frame}
\frametitle{$\Lo_r$ is decidable in \evol{2}}

 \begin{center}
  The algorithm exploits the theory of Well Structured Transition Systems
 \end{center}

This accounts for:
\begin{enumerate}
 \item  defining an ordering on states 
\vspace{0.2cm}
\item performing a symbolic backward analysis
\begin{center}
\includegraphics[width=0.5\textwidth]{predanalisi.pdf} 
\end{center}

\item Check whether it is  possible to \emphcolor{reach a
process greater} than one that exhibit at least $k$ signals

\end{enumerate}


\end{frame}

\begin{frame}
\frametitle{The table:} 
\begin{center}
\begin{tabular}{c|c|c}
		& $\Lo$ & $\Lo_r$ \\
\hline \hline
\evol{1}	&~  undec ~& ~ undec~\\
\hline
\evol{2}	& ~ undec ~ & ~ dec~ \\
%\OG~dec~/~\LG dec 
\end{tabular}
\end{center}

\end{frame}

\section{Type system}

\begin{frame}
 \frametitle{Type system}
 
 We want to guarantee consistent updates:
 \begin{itemize}
  \item no communication/protocol is interrupted by an update \\ (\emphcolor{session types})
  \vspace{0.5cm}
  \item updates are regulated \\ (\emphcolor{process interface})
 \end{itemize}

 
\end{frame}

\begin{frame}
\frametitle{Sessions -- 1}

\begin{itemize}
 
 \item Sessions abstract communication protocols 
 \vspace{0.5cm}
 \item They represent contracts, i.e. sequences of communications along a channel.

\end{itemize}

\begin{block}{}
$$P::= \dots  \, \mid \, \open{c:\rho}.P \, \mid \, \close{c}.P$$
\end{block}

\end{frame}


\begin{frame}
\frametitle{Sessions -- 2 }

\begin{example}
$$P_1 :=  \open{c:\rho}.\outC{c}.c.\close{c}$$ 
\end{example}

\pause

\begin{itemize}
 \item In order to work, a session needs a dual. 
\end{itemize}

\pause

\begin{example}
$$P_2 :=  \open{c:\overline{\rho}}.c.\outC{c}.\close{c}$$ 
\end{example}

\end{frame}

\begin{frame}
\frametitle{Identify active sessions}

\begin{itemize}

 \item Adaptable processes record the number of active sessions 
\end{itemize}

\begin{example}
$$
\begin{array}{l}
\component{m^0}{\open{c:\rho}.P} \parallel \component{n^0}{\open{c:\overline{\rho}}.Q}   \pired\\
\\
\component{m^1}{P} \parallel \component{n^1}{Q}   
\end{array}
$$
\end{example}



\end{frame}



\begin{frame}
\frametitle{Session types}


\begin{itemize}
  \item Typing guarantees that no session is interrupted by an update (\emphcolor{Session consistency}) 
\end{itemize}

\pause
\begin{block}{Type judgment}

$$
\begin{array}{ccccccc}
\text{First}&&
&& \text{Active }\\
 \text{order} &&&& \text{sessions}\\
 \text{envir}\\

\Gamma &;& \Theta &\vdash P:: & \Phi &;& \Delta \\ 

&& \text{Higher order} &&&& \text{Non active }\\
&& \text{environment} &&&& \text{sessions}
\end{array}
$$
\end{block}


\end{frame}

\begin{frame}

\frametitle{Some rules}

$$
\begin{array}{lc}
\rulename{t:Open} &
\cfrac{
\begin{array}{c}
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Phi, c:\rho_\qua}{\,\Delta}} 
%\mathsf{cond}(\Delta, \Delta_l, \Delta_u,  \Theta, \rho)
\end{array}
}{\judgebis{\env{\Gamma}{\Theta}}{\open{c:\rho_\qua}.P}{ \type{\Phi}{\,\Delta \addelta \rho_\qua}}} \\

\\
\rulename{t:Par} &
\cfrac{
\begin{array}{l}
\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Phi_1}{ \Delta_1}} \\
 \judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\Phi_2}{ \Delta_2}}
\end{array}
 \quad 
\begin{array}{l}
\Phi = \Phi_1 \bowtie \Phi_2 \\ \Delta = \Delta_1 \addelta \Delta_2
\end{array}}{\judgebis{\env{\Gamma}{\Theta}}{P \parallel Q}{\type{\Phi}{\Delta}}}\\

\\

\rulename{t:Loc} & \cfrac{\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Phi}{\Delta}} \qquad h = \#\{c \mid c:\omega \in \Phi\} }{\judgebis{\env{\Gamma}{\Theta}}{\component{l^h}{P} }{ \type{\Phi}{\Delta}}}\\
\\
%\rulename{t:Upd}   & 
%\cfrac{\judgebis{\env{\Gamma}{\Theta,\mathsf{X}:{\Delta_1}}}{P}{\type{\emptyset}{ \Delta_2 }}}{\judgebis{\env{\Gamma}{\Theta}}{\updated{l}{X}{\Delta_1}{\Delta_2}{P}}{\type{\emptyset}{ \emptyset}}}
\end{array}
$$

\end{frame}

\begin{frame}

\frametitle{Subject reduction}

\begin{theorem}
\begin{center}
If $\judgebis{\env{\Gamma}{\Theta}}{P}{\type{\Phi}{\Delta}}$ and $P \pired Q$ then\\
\quad \\
 $\judgebis{\env{\Gamma}{\Theta}}{Q}{ \type{\Phi'}{\Delta'}}$, for some $\Phi', \Delta'$.
 \end{center}
\end{theorem}

\end{frame}





\begin{frame}
 \frametitle{Interfaces -- 1}
 
 \begin{itemize}
  \item How can we regulate updates?
  \vspace{0.5cm}
  \pause
  \item We treated updates as functions: i.e. updates can be applied only if the adaptable process has a compatible \emphcolor{interface}.
  \vspace{0.5cm}
  
\pause  
  \item Interfaces records the \emphcolor{abilities} of a process i.e. not yet opened sessions 
  
  
 \end{itemize}
 
 
\end{frame}


\begin{frame}
\frametitle{Interfaces -- 2}

\begin{example}
$$
\component{m^0}{\open{c:\rho}.P} \parallel 
\mupdate{m}{Q}{\Delta_1}{\Delta_2} 
$$
\end{example}

\pause
\vspace{0.5cm}
$$
\begin{array}{lc}

\rulename{t:Upd}   & 
\cfrac{\judgebis{\env{\Gamma}{\Theta,\mathsf{X}:{\Delta_1}}}{P}{\type{\emptyset}{ \Delta_2 }}}{\judgebis{\env{\Gamma}{\Theta}}{\updated{l}{X}{\Delta_1}{\Delta_2}{P}}{\type{\emptyset}{ \emptyset}}}
\end{array}
$$
\end{frame}



\section{Conclusions}


\begin{frame}
 \frametitle{Summing up \dots}
 
\begin{itemize}
\item A process calculus approach to dynamic reconfiguration, evolvability, and adaptation
\vspace{0.5cm}
\item 
A basis for the development of more expressive languages, and for verification studies
\vspace{0.5cm}
\item 
A simple logic for expressing adaptation properties
of evolvable systems
\end{itemize}


\end{frame}

\begin{frame}
\frametitle{Future works}

Typing system:
\begin{itemize}
 
 \item Obtaining progress: i.e. sessions are not deadlocked.

\vspace{0.5cm} 
 
 \item Refine the notion of process interface and interface compatibility.
  
\vspace{0.5cm }  
  
 \item Refine the notion of transparent location.
 
\end{itemize}
 
 
 
\end{frame}









\begin{frame}
\begin{center}
 \emphcolor{Thanks!}
\end{center}
\end{frame}


\end{document}
